#ifndef MINISAT_H_
#define MINISAT_H_

#include "Graph.h"

/* Minsat encapsule l'exectution du programme minisat
 * sur des graphes qui doivent etre une instance correcte
 * du probleme Vertex Cover.                              */

/* Usage :
 * 		1 - Créer une instance de l'objet Minisat avec ou sans
 * 			graphe (Graph) en parametre.
 * 		2 - Si aucun graphe (Graph) n'a été passé en parametre
 * 			lors de la création, en définir un avec la methode
 * 			setProblem(Graph).
 * 		3 - Lancer l'evaluation du graphe par Minisat avec la
 * 			methode eval().
 * 			/!\ cette etape est codée en dur et necessite
 * 			qu'un executable de Minisat nommé "minisat_static"
 * 			soit présent dans le dossier.
 * 		4 - Recuperer le résultat retourné sous forme d'une
 * 			liste de sommets appartenant à la couverture par
 * 			la methode getSolution()
 */

using namespace std;

class SAT {
private:
	bool _evaluated;
	bool _solvable;
	int _nb_variables;
	vector<pair<int,int> > _problem;
	vector<int> _solution;

	void writeInfile();
	void runMinisat();
	void readOutfile();
public:
	SAT();
	SAT(vector<pair<int,int> >);
	virtual ~SAT();
	void add(pair<int,int>);
	void add(int,int);
	void setNbVariables(int n);
	int getNbVariables();
	vector<int> getSolution();
	void eval();
	bool evaluated();
	bool solvable();
};

class Minisat {
private:
	SAT* _sat;

	SAT* 	VC2SAT(Graph);
	vector<int>	SAT2VC(SAT*);
public:
	// Constructeur (default)
	Minisat();
	Minisat(Graph);
	virtual ~Minisat();

	// Definit le Graph du probleme VC
	void 	setProblem(Graph);

	// evalue SAT
	void 	eval();

	// Transforme la solution de minisat en Graph
	// SAT doit avoir été evalué
	vector<int>	getSolution();

	// Evalue le Graph passé en parametre
	// Retourne un Graphe corespondant a une solution
	// fourni par minisat executé sur le graphe initial
	// NB : Ceci est une concatenation des 3 fonction
	// setProblem, eval, getSolution
	vector<int>	runMinisatOn(Graph);
};

#endif
